Formal Verification of Consensus Algorithms
Blockchain
Nakamoto consensus
George Pirlea, Ilya Sergey (University College London, UK) Based on FACTum, which is based on Isabelle/HOL The proved property: blockchain integrity, i.e., that additions to the blockchain are guaranteed to be persistent.
Similar to common prefix
Consideration of attackers
Max DiGiacomo-Castillo, Yiyun Liang, Advay Pal, John C. Mitchell (Stanford)
UPPAAL-SMC
Analyzing Selfish mining
Ouroboros
Forkable Strings of ouroboros paper in Isabelle/HOL
Kawin Worrasangasilpa
psi calculus: a generalization of the pi calculus with more advanced features
we can embed (shallow-embedding?) it as a domain-specific language (DSL) in Haskell and:
both execute and run (it’s just Haskell after all)
test using QuickCheck (Haskell’s randomized testing tool)
do formal verification using the psi calculus metatheory.
Søren Eller Thomsen and Bas Spitters
Safety and Liveness of a protocol similat to Ouroboros Praos
Casper FFG
Runtime Verification
Verification of previous version of Casper FFG with Isabelle by Yoichi Hirai
Alloy, Isabelle
Runtime Verification
CBC Casper
Algorand
GitHub by Runtime Verification Stellar Consensus Protocol
Verification with Isabelle and Ivy Formalizes some definitions and proofs of the Stellar whitepaper and a simpler take on federated voting in Isabelle
Formalizes and proves safety of the ballot protocol in Ivy
Junghun Yoo (University of Oxford) et al.
Stellar Consensus Protocol in UPPAAL
Pierre Tholoniat (University of Sydney), Vincent Gramoli (University of Sydney)
Verify Two components of Red Belly Blockchain using the ByMC model checker
1. A simple broadcast primitive
2. A blockchain consensus algorithm written in 309
Others
Formal verification of fairness of the Tendermint proposer election algorithm
Traditional BFT
Velisarios
ESOP'18
Vincent Rahli et al. (University of Luxembourg)
A logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols
Extends the Logic of Events (LoE) in order to reason not only about crash faults, but also about arbitrary faults.
In LoE, an event is an abstract entity that corresponds either (1) to the handling of a received message, or (2) to some arbitrary activity about which no information is provided.
As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area’s reference protocol: PBFT. (See Velisarios/PBFT) proved only safety
https://gyazo.com/4d01242baf866458468d6f205f68e6b6
Others
Develop a methodology for deductive verification of thresholdbased distributed protocols using decidable logic
Decomposition into two well-established decidable logics
Implemented with Z3 and CVC4
Verified Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos
Traditional CFT
Verdi
A framework for formally verifying distributed systems implementations in Coq
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas Anderson (University of Washington, USA)
cited 118
Contribution from Karl Palmskog
Verdi Raft
proved only safety
Verdi currently supports verifying safety properties, but not liveness properties, and none of Verdi’s network semantics currently capture Byzantine fault models. We believe that Verdi could be extended to support these features: liveness properties could be verified by supporting infinite traces and adding fairness hypotheses as axioms as in TLA, while Byzantine fault models can be supported by adding more non-determinism in the network semantics.
Verdi Chord
DISEL
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Ilya Sergey (University College London, UK)
James R. Wilcox, Zachary Tatlock (University of Washington, USA)
Contribution from Karl Palmskog
Ivy
See Ivy about the tool itself Deductive verification based on effectively propositional logic (EPR)
A decidable fragment of first-order logic (also known as the Bernays-Schönfinkel-Ramsey class).
The finite model property, allowing to display violations as finite structures which are intuitive for users.
Modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check.
The steps of the transformations are also mechanically checked, ensuring the soundness of the method
Paxos and its variants
Implemented in Ivy
EventML
Vincent Rahli (Cornell University)
A language for implementing distributed systems
Nicolas Schiper Vincent Rahli Robbert Van Renesse Mark Bickford Robert L. Constable (Cornell University)
from Verdi Raft's paper
EventML programs can be verified in NuPRL using the Logic of Events.
EventML and the Logic of Events have been used to verify an implementation of Multi-Paxos, a total-order broadcast service, used as part of a distributed database
IronFleet
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, Brian Zill (Microsoft Research)
cited 134
TLA-style state-machine refinement and Hoare-logic verification (Dafny, an SMT-based program verification toolchain) from Verdi Raft's paper,
This approach enables building practical distributed systems and proving both safety and, unlike our Raft proof in Verdi, liveness properties.
Also unlike our Raft implementation in Verdi, IronFleet’s implementation of Paxos supports many important practical features including verified marshaling and parsing, state transfer, and log truncation
Head-Of model
Bernadette Charron-Bost (Ecole polytechnique), Andr´e Schiper (EPFL)
Henri Debrat (Universit´e de Lorraine & LORIA) and Stephan Merz (Inria Nancy Grand-Est & LORIA)
Formalize Heard-Of model in Isabelle/HOL the
HO model can represent algorithms that operate in communication-closed rounds, which is true of virtually all known fault-tolerant distributed algorithms.
Both safety and liveness
Extenstion for Byzantine faults
Martin Biely (TU Wien) et al.
DSL based on Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages
Paxos
Does not deal with Byzantine faults
Ognjen Maric, Christoph Sprenger, and David Basin (ETH Zurich)
Ognjen Maric, Christoph Sprenger, and David Basin (ETH Zurich)
Define a language ConsL, capable of expressing numerous consensus algorithms (Paxos, Chandra-Toueg, Ben-Or etc.)
Leverage model checking to provide the first fully automated decision procedure applicable to a range of consensus algorithms (Promela/Spin)
Other Isabelle/HOL works
From TLA+ specification to Isabelle
Model checking of traditional protocols
TLA+
Paxos
Leslie Lamport
SPIN
Paxos
Giorgio Delzanno et.al.
SMV
Non-probabilistic Verification: the verification of Validity and Agreement and the non-probabilistic arguments for proving Probabilistic wait-free termination using Cadence SMV
Probabilistic Verification: the verification of the probabilistic arguments for proving Probabilistic wait-free termination using PRISM
Related/Others
Miguel Castro (MIT)
Formal proof of safety and liveness of pBFT using I/O automata
Emmanuelle Anceaume (IRISA) et al.
Bitcoin, GHOST, Byzcoin, Algorand, PeerCensus, Red Belly
Yoichi Hirai